Nuprl Definition : finite-type
0,22
postcript
pdf
finite-type(
T
) ==
n
:
,
f
:(
n
T
). Surj(
n
;
T
;
f
)
latex
clarification:
finite-type(
T
) ==
n
:
,
f
:({0..
n
}
T
). Surj({0..
n
};
T
;
f
)
latex
Definitions
{
i
..
j
}
,
Surj(
A
;
B
;
f
)
,
x
:
A
.
B
(
x
)
,
FDL editor aliases
finite-type
origin
n:
, f:(n
T). Surj(n; T; f)
n:, f:({0..n
}T). Surj({0..n}; T; f) n:, f:(nT). Surj(n; T; f)
n:, f:({0..n}T). Surj({0..n}; T; f) }x:A. B(x)